%==============================================================================
% Enunciado
%==============================================================================

% Formalizar en OTTER la siguiente argumentación y comprobar su validez:
% "Sólo las buenas personas ayudan a los pobres. Ninguna buena persona es
% aficionada a la fotografía. Antonio ayuda a Juan y es aficionado a la
% fotografía. Luego Juan no es pobre."

%==============================================================================
% Formalización
%==============================================================================

set(auto2).

formula_list(sos).
% Solo las buenas personas ayudan a los pobres.
  all x y (ayuda(x,y) & esPobre(y) -> buenaPersona(x)).
% Es equivalente a la siguiente:
  all x y (-buenaPersona(x) & esPobre(y) -> -ayuda(x,y)).

% Esta formulación es incorrecta.
%   all x y (buenaPersona(x) & esProbre(y) -> ayuda(x,y)).

% Ninguna buena persona es aficionada a la fotografía.
  all x (buenaPersona(x) -> -aficionadoFotografia(x)).
% Es equivalente a la siguiente:
%   - exists x (buenaPersona(x) & aficionadoFotografia(x)).

% Antonio ayuda a Juan y es aficionado a la fotografía.
  ayuda(Antonio,Juan).
  aficionadoFotografia(Antonio).

% Conclusión: Juan no es pobre.
  esPobre(Juan).
end_of_list.

%==============================================================================